Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning

摘要

This paper defines the (first-order) conflict resolution calculus: anextension of the resolution calculus inspired by techniques used in modernSAT-solvers. The resolution inference is restricted to (first-order)unit-propagation and the calculus is extended with a mechanism for assumingdecision literals and a new inference rule for clause learning, which is afirst-order generalization of the propositional conflict-driven clause learning(CDCL) procedure. The calculus is sound (because it can be simulated by naturaldeduction) and refutationally complete (because it can simulate resolution),and these facts are proven in detail here.